$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{B}$), ${\it as}$:$T$ List.
\\[0ex]($\exists$$a$:$T$. ($a$ $\in$ ${\it as}$) \& $P$($a$))
\\[0ex]$\Rightarrow$ hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ $T$ \& (hd(filter($\lambda$$a$.$P$($a$);${\it as}$)) $\in$ ${\it as}$) \& $P$(hd(filter($\lambda$$a$.$P$($a$);${\it as}$)))